Thanks, Matthias. I am puzzled that I am not getting these errors regardless of the '-Werror' option. Probably, it has to do with using 32-bit Ubuntu. I will make the necessary changes. Eugene

I committed the required changes. Eugene

Done. Eugene

Yes, it did. Eugene

I cannot make ebmc, now. Should I pull the latest version of 'cbmc'? Eugene

I just compiled EBMC with ic3_bugs rebased onto master on a 32-Bit BSD and I now get the same as you for property 1 and a segmentation fault for property 2 ``` openbsdy% ebmc --bound 10 example3.sv --ic3 --property counter.property.1 Parsing example3.sv Converting Type-checking Verilog::counter Using module `counter' Generating Netlist verification of properties of this type by IC3 is not implemented yet openbsdy% ebmc --bound 10 example3.sv --ic3 --property counter.property.2 Parsing example3.sv Converting Type-checking Verilog::counter Using module `counter' Generating Netlist zsh: segmentation fault (core dumped) ebmc --bound 10 example3.sv --ic3 --property counter.property.2 ``` could this be someting dependent on 32/64 bit ?

Hi Matthias, 1) I am still getting the same result after rebasing and cleaning and recompiling cbmc and ebmc. (I attached the example I ran and the output produced by running 'ebmc --example3.sv --ic3 --property counter.property.2". Adding "--bound 10" does not change anything. could this be someting dependent on 32/64 bit ? 2) I have no clue yet. Could you run 'ebmc --example3.sv --bound 10 --property counter.property.2" to rule out that anything bad happens before ic3 is called? Eugene

Parsing example3.sv Converting Type-checking Verilog::counter Using module `counter' Generating Netlist adding 0 unit constraints ------------- next_time_frame tf_lind = 1 F.size() = 8, #inact. clauses 0 Time frame SAT-solvers: 9 calls Push clause SAT-solving: 0 calls property FAILED Cex.size() = 4 cex verification is ok ********* num of time frames = 1 #inputs = 2, #outputs = 1, #latches = 8, #gates = 83 total number of generated clauses is 1 orig_ind_cls = 1, succ_impr = 0, failed_impr = 0 Aver. clause size = 0.0 max. num. improv. of an ind. clause is 0 #add1 = 0, #add2 = 0, #replaced = 0, #restore = 0 Gen_sat: 10 calls Bst_sat: 1 calls Lbs_sat: 1 calls Lgs_sat: 3 calls Time frame SAT-solvers: 9 calls Push clause SAT-solving: 0 calls all solvers: 24 calls rem_subsumed_flag = 1 lit_pick_heur = INACT_VAR act_upd_mode = MINISAT_ACT_UPD sorted objects = VARS lift_sort_mode = FULL_SORT ind_cls_sort_mode = FULL_SORT gate_sort_mode = INPS_FIRST selector = 0 ctg_flag = 1 constr_flag = 0 standard_mode = 1 muliplier = 1.05 #svars = 8, aver. bst. cube = 8.0, aver. gst. cube = 8.0 root_state_cnt = 1, new_state_cnt = 2, old_state_cnt = 1 (triv = 0, rem = 1) #CTGs = 0, #excluded CTGS = 0 total time is 0.00 sec.

Hi Eugene,

``` openbsdy% ebmc example3.sv --bound 10 --property counter.property.2 Parsing example3.sv Converting Type-checking Verilog::counter Using module `counter' Using MiniSAT 2.2.1 with simplifier Generating Decision Problem General constraints Initial state Transition relation Transition 0->1 Transition 1->2 Transition 2->3 Transition 3->4 Transition 4->5 Transition 5->6 Transition 6->7 Transition 7->8 Transition 8->9 Transition 9->10 Transition 10 Solving with propositional reduction Checking counter.property.2 353 variables, 1136 clauses SAT checker: instance is SATISFIABLE SAT: counterexample found ** Results: [counter.property.2] always counter.state != 3: FAILURE ``` this works as intended. I get the following stacktrace ``` openbsdy% gdb ebmc GNU gdb 6.3 Copyright 2004 Free Software Foundation, Inc. GDB is free software, covered by the GNU General Public License, and you are welcome to change it and/or distribute copies of it under certain conditions. Type "show copying" to see the conditions. There is absolutely no warranty for GDB. Type "show warranty" for details. This GDB was configured as "i386-unknown-openbsd6.1"... (gdb) run example3.sv --bound 10 --property counter.property.2 --ic3 Starting program: /usr/local/bin/ebmc example3.sv --bound 10 --property counter.property.2 --ic3 Parsing example3.sv Converting Type-checking Verilog::counter Using module `counter' Generating Netlist Program received signal SIGSEGV, Segmentation fault. 0x19e7e980 in std::vector<int, std::allocator<int> >::_M_fill_assign () from /usr/local/bin/ebmc (gdb) bt #0 0x19e7e980 in std::vector<int, std::allocator<int> >::_M_fill_assign () from /usr/local/bin/ebmc #1 0x19e9ab66 in CompInfo::assign_var_indexes () at minisat/core/Solver.cc:103 #2 0x19e95c07 in CompInfo::gen_cnfs () at minisat/core/Solver.cc:103 #3 0x19e84d6b in ic3_enginet::read_ebmc_input () from /usr/local/bin/ebmc #4 0x19e70de1 in ic3_enginet::operator() () from /usr/local/bin/ebmc #5 0x19e70ce1 in do_ic3 () from /usr/local/bin/ebmc #6 0x19d20904 in ebmc_parse_optionst::doit () from /usr/local/bin/ebmc #7 0x19d4f2da in parse_options_baset::main () from /usr/local/bin/ebmc #8 0x19d0c05a in main () from /usr/local/bin/ebmc ``` Best, Matthias

Hi Eugene, did you push the rebased branch `ic3_bugs`? What I see on github says https://github.com/diffblue/hw-cbmc/tree/ic3_bugs "This branch is 16 commits ahead, 10 commits behind master." We risk trying different versions here. Best, Matthias

Hi Matthias, Please try now. Best wishes, Eugene

Hi Matthias, Now the ic3_bugs branch is ahead of the master. Could you please check if the problem with the counter example still persists? Eugene

Hi Eugene, yes, works now as intended, property.1 is not yet implemented and property.2 is proven. Best, Matthias

Hi Matthias, No problem. I can make the required changes. First, I need to get a version of ebmc that compiles. Eugene

Hi Matthias, How do I get a version of ebmc that compiles? Can someone just modify the backport_to_cbmc_5.6 branch by removing 'pragma*def' includes? Daniel says that he has done precisely that but it looks like this change has not been committed yet. Eugene

with Daniel's changes and the correct submodule pointer I should correctly build EBMC I'd also like to see all `int` being of `unsigned` type where possible, but this would likely require more time. In my opinion, for the release we should include ic3, but make it fail gracefully for the unsupported cases and transform the C-style I/O and fixed arrays which is prone to result in problems.

Hi Matthias, Could you please send me the 'test.smv' file you threw at ic3? Best wishes, Eugene

Hi Eugene, it is just the `BDD5` regression test `main.smv` where ``` ebmc --ic3 main.smv ``` fails with ``` Parsing main.smv Converting Type-checking smv::main Generating Netlist terminate called after throwing an instance of 'std::invalid_argument' what(): stoi fish: “ebmc --ic3 main.smv” terminated by signal SIGABRT (Abort) ```

Hi Matthias, 1) Things look different in branch 'new_ic3_bugs'. The 'main.smv' example of BDD5 just breaks assertion assert (Prop.expr.id()==ID_sva_always); However, when I relaxed this assertion into assert ((Prop.expr.id()==ID_sva_always) || (Prop.expr.id() == ID.AG)); the example went through. (Safety properties of verilog and smv files have different identifications.) 2) Inspired by this example, I checked all smv files of 'regression/ebmc'. Unfortunately, some of them do not go through. My guess is that there are some subtle differences in how networks are generated from Verilog and smv descriptions. So using ic3 to solve AG properties of smv designs is quite doable. 3) For now, I will limit the properties handled by IC3 to ID_sva_always. Best wishes, Eugene